g:IAbGrp{i}, a, b:|g|. (a * ((~(a)) * b)) = b & ((~(a)) * (a * b)) = b 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup, IAbGrp{i}
Definitions	t  T, x:A. B(x), P  Q, P  Q, P  Q, x f y, P & Q, IMonoid, IGroup, IAbGrp{i}
Lemmas	iabgrp wf, grp car wf, grp inverse, grp op wf, grp inv wf, mon assoc, mon ident